1  /-
  2  Copyright (c) 2018 Mario Carneiro and Kevin Buzzard. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Mario Carneiro, Kevin Buzzard
  5  -/
  6  
  7  import data.equiv.algebra
src         └────────────────┘
  8  import linear_algebra.finsupp
src         └────────────────────┘
  9  import ring_theory.ideal_operations
src         └──────────────────────────┘
 10  import ring_theory.subring
src         └─────────────────┘
 11  import linear_algebra.basis
src         └──────────────────┘
 12  
 13  open set lattice
 14  
 15  namespace submodule
 16  variables {α : Type*} {β : Type*} [ring α] [add_comm_group β] [module α β]
id                                                    └───────┘     └────┘
src                                                   └───────┘     └────┘
typ                                                   └───────┘     └────┘
doc                                                                 └────┘
 17  
 18  def fg (s : submodule α β) : Prop := ∃ t : finset β, submodule.span α ↑t = s
id               └───────┘                   └────┘  └────────────┘    
src              └───────┘                     └────┘   └────────────┘     
typ              └───────┘                   └────┘  └────────────┘    
doc              └───────┘                      └────┘    └────────────┘
 19  
 20  theorem fg_def {s : submodule α β} :
id                       └───────┘  
src                      └───────┘
typ                      └───────┘  
doc                      └───────┘
 21    s.fg ↔ ∃ t : set β, finite t ∧ span α t = s :=
id     └─┘       └─┘  └────┘   └──┘    
src     └─┘       └─┘   └────┘    └──┘     
typ    └─┘       └─┘  └────┘   └──┘    
doc                        └────┘     └──┘
 22  ⟨λ ⟨t, h⟩, ⟨_, finset.finite_to_set t, h⟩, begin
id               └──────────────────┘
src                 └──────────────────┘
typ              └──────────────────┘
st                                              └─────
 23    rintro ⟨t', h, rfl⟩,
src    └─────────────────┘
typ    └─────────────────┘
doc    └─────────────────┘
txt    └─────────────────┘
par    └─────────────────┘
pid          └───────────┘
st   ────────────────────┘└─
 24    rcases finite.exists_finset_coe h with ⟨t, rfl⟩,
id            └──────────────────────┘ 
src    └─────┘└──────────────────────┘ └────────────┘
typ    └─────┘└──────────────────────┘└────────────┘
doc    └─────┘                         └────────────┘
txt    └─────┘                         └────────────┘
par    └─────┘                         └────────────┘
pid                                   └────────────┘
st   ────────────────────────────────────────────────┘└─
 25    exact ⟨t, rfl⟩
id              └─┘
src    └────┘  └┘└─┘└┘
typ    └────┘ └┘└─┘└┘
doc    └────┘  └┘   └┘
txt    └────┘  └┘   └┘
par    └────┘  └┘   └┘
pid           └┘   
st   ────────────────┘
 26  end⟩
st   └─┘
 27  
 28  /-- Nakayama's Lemma. Atiyah-Macdonald 2.5, Eisenbud 4.7, Matsumura 2.2, Stacks 00DV -/
 29  theorem exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul {R : Type*} [comm_ring R]
id                                                                             └───────┘ 
src                                                                            └───────┘
typ                                                                            └───────┘ 
 30    {M : Type*} [add_comm_group M] [module R M]
id                  └────────────┘    └────┘  
src                 └────────────┘     └────┘
typ                 └────────────┘    └────┘  
doc                                    └────┘
 31    (I : ideal R) (N : submodule R M) (hn : N.fg) (hin : N ≤ I • N) :
id          └───┘        └───────┘          └─┘             
src         └───┘         └───────┘             └─┘              
typ         └───┘        └───────┘          └─┘             
doc                       └───────┘
 32    ∃ r : R, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = (0 : M) :=
id                                  
src                                 
typ                                 
 33  begin
 34    rw fg_def at hn, rcases hn with ⟨s, hfs, hs⟩,
src    └─┘      └────┘  └─────┘  └────────────────┘
typ    └─┘      └────┘  └─────┘  └────────────────┘
doc    └─┘      └────┘  └─────┘  └────────────────┘
txt    └─┘      └────┘  └─────┘  └────────────────┘
par    └─┘      └────┘  └─────┘  └────────────────┘
pid            └────┘          └────────────────┘
 35    have : ∃ r : R, r - 1 ∈ I ∧ N ≤ (I • span R s).comap (linear_map.lsmul R M r) ∧ s ⊆ N,
id                                                          └──────────────┘          
src    └─────┘ └───┘    └─┘             └──────┘ └──────────────┘   └┘  
typ    └─────┘ └───┘    └─┘             └──────┘ └──────────────┘ └┘ 
doc    └─────┘ └───┘    └─┘             └──────┘                    └┘   
txt    └─────┘ └───┘    └─┘              └──────┘                    └┘   
par    └─────┘ └───┘    └─┘              └──────┘                    └┘   
pid    └───┘└┘ └───┘    └─┘              └──────┘                    └┘   
st                                             └───────────────────────────────────────────┘└─
 36    { refine ⟨1, _, _, _⟩,
src      └─────┘ └─────────┘
typ      └─────┘ └─────────┘
doc      └─────┘ └─────────┘
txt      └─────┘ └─────────┘
par      └─────┘ └─────────┘
pid             └─────────┘
st   ───┘└─────────────────┘└─
 37      { rw sub_self, exact I.zero_mem },
id            └──────┘        └────────┘
src        └─┘└──────┘  └────┘└────────┘
typ        └─┘└──────┘  └────┘└────────┘
doc        └─┘          └────┘          
txt        └─┘          └────┘          
par        └─┘          └────┘          
pid                                   
st   ─────┘└─────────┘└─────────────────┘└┘
 38      { rw [hs], intros n hn, rw [mem_coe, mem_comap], change (1:R) • n ∈ I • N, rw one_smul, exact hin hn },
id             └┘                    └─────┘  └───────┘                            └──────┘        └─┘ └┘
src        └──┘    └─────────┘  └──┘└─────┘└┘└───────┘  └─────┘ └┘ └┘        └─┘└──────┘  └────┘     
typ        └──┘└┘  └─────────┘  └──┘└─────┘└┘└───────┘  └─────┘ └┘└┘     └─┘└──────┘  └────┘└─┘└┘
doc        └──┘    └─────────┘  └──┘       └┘           └─────┘ └┘ └┘        └─┘          └────┘     
txt        └──┘    └─────────┘  └──┘       └┘           └─────┘ └┘ └┘        └─┘          └────┘     
par        └──┘    └─────────┘  └──┘       └┘           └─────┘ └┘ └┘        └─┘          └────┘     
pid          └┘          └───┘    └┘       └┘                  └┘ └┘                              
st   ─────┘└────┘└────────────┘└───────────┘└─────────┘└─────────────────────────┘└───────────┘└─────────────┘└┘
 39      { rw [← span_le, hs], exact le_refl N } },
id               └─────┘  └┘         └─────┘ 
src        └────┘└─────┘└┘    └────┘└─────┘ 
typ        └────┘└─────┘└┘└┘  └────┘└─────┘
doc        └────┘       └┘    └────┘        
txt        └────┘       └┘    └────┘        
par        └────┘       └┘    └────┘        
pid          └──┘       └┘                 
st   ──────────────────┘└──┘└─────────────────┘└──┘
 40    clear hin hs, revert this,
src    └──────────┘  └─────────┘
typ    └──────────┘  └─────────┘
doc    └──────────┘  └─────────┘
txt    └──────────┘  └─────────┘
par    └──────────┘  └─────────┘
pid         └─────┘        └───┘
st   ─────────────┘└───────────┘└─
 41    refine set.finite.dinduction_on hfs (λ H, _) (λ i s his hfs ih H, _),
id            └──────────────────────┘ └─┘
src    └─────┘└──────────────────────┘     └─────┘  └───────────────────┘
typ    └─────┘└──────────────────────┘└─┘  └─────┘  └───────────────────┘
doc    └─────┘                             └─────┘  └───────────────────┘
txt    └─────┘                             └─────┘  └───────────────────┘
par    └─────┘                             └─────┘  └───────────────────┘
pid                                       └─────┘  └───────────────────┘
st   ─────────────────────────────────────────────────────────────────────┘└─
 42    { rcases H with ⟨r, hr1, hrn, hs⟩, refine ⟨r, hr1, λ n hn, _⟩, specialize hrn hn,
id                                                 └─┘                         └─┘ └┘
src      └─────┘ └─────────────────────┘  └─────┘  └┘   └┘ └───────┘  └─────────┘   
typ      └─────┘└─────────────────────┘  └─────┘ └┘└─┘└┘ └───────┘  └─────────┘└─┘└┘
doc      └─────┘ └─────────────────────┘  └─────┘  └┘   └┘ └───────┘  └─────────┘   
txt      └─────┘ └─────────────────────┘  └─────┘  └┘   └┘ └───────┘  └─────────┘   
par      └─────┘ └─────────────────────┘  └─────┘  └┘   └┘ └───────┘  └─────────┘   
pid             └─────────────────────┘          └┘   └┘ └───────┘               
st   ───┘└─────────────────────────────┘└──────────────────────────┘└─────────────────┘└─
 43      rwa [mem_coe, mem_comap, span_empty, smul_bot, mem_bot] at hrn },
id            └─────┘  └───────┘  └────────┘  └──────┘  └─────┘
src      └───┘└─────┘└┘└───────┘└┘└────────┘└┘└──────┘└┘└─────┘└───────┘
typ      └───┘└─────┘└┘└───────┘└┘└────────┘└┘└──────┘└┘└─────┘└───────┘
doc      └───┘       └┘         └┘          └┘        └┘       └───────┘
txt      └───┘       └┘         └┘          └┘        └┘       └───────┘
par      └───┘       └┘         └┘          └┘        └┘       └───────┘
pid         └┘       └┘         └┘          └┘        └┘       └─────┘
st   ───────────────┘└─────────┘└──────────┘└────────┘└───────┘└──────┘└┘
 44    apply ih, rcases H with ⟨r, hr1, hrn, hs⟩,
id                      
src    └────┘    └─────┘ └─────────────────────┘
typ    └────┘    └─────┘└─────────────────────┘
doc    └────┘    └─────┘ └─────────────────────┘
txt    └────┘    └─────┘ └─────────────────────┘
par    └────┘    └─────┘ └─────────────────────┘
pid                    └─────────────────────┘
st   ─────────┘└───────────────────────────────┘└─
 45    rw [← set.singleton_union, span_union, smul_sup] at hrn,
id           └─────────────────┘  └────────┘  └──────┘
src    └────┘└─────────────────┘└┘└────────┘└┘└──────┘└──────┘
typ    └────┘└─────────────────┘└┘└────────┘└┘└──────┘└──────┘
doc    └────┘                   └┘          └┘        └──────┘
txt    └────┘                   └┘          └┘        └──────┘
par    └────┘                   └┘          └┘        └──────┘
pid      └──┘                   └┘          └┘        └─────┘
st   ──────────────────────────┘└──────────┘└────────┘└─────┘└─
 46    rw [set.insert_subset] at hs,
id         └───────────────┘
src    └──┘└───────────────┘└─────┘
typ    └──┘└───────────────┘└─────┘
doc    └──┘                 └─────┘
txt    └──┘                 └─────┘
par    └──┘                 └─────┘
pid      └┘                 └────┘
st   ──────────────────────┘└────┘└─
 47    have : ∃ c : R, c - 1 ∈ I ∧ c • i ∈ I • span R s,
id                                         └──┘  
src    └─────┘└───┘   └─┘         └──┘ 
typ    └─────┘└───┘   └─┘       └──┘
doc    └─────┘ └───┘    └─┘         └──┘ 
txt    └─────┘ └───┘    └─┘              
par    └─────┘ └───┘    └─┘              
pid    └───┘└┘ └───┘    └─┘              
st   ─────────────────────────────────────────────────┘└─
 48    { specialize hrn hs.1, rw [mem_coe, mem_comap, mem_sup] at hrn,
id                  └─┘ └┘        └─────┘  └───────┘  └─────┘
src      └─────────┘     └┘  └──┘└─────┘└┘└───────┘└┘└─────┘└──────┘
typ      └─────────┘└─┘└┘└┘  └──┘└─────┘└┘└───────┘└┘└─────┘└──────┘
doc      └─────────┘     └┘  └──┘       └┘         └┘       └──────┘
txt      └─────────┘     └┘  └──┘       └┘         └┘       └──────┘
par      └─────────┘     └┘  └──┘       └┘         └┘       └──────┘
pid                     └┘    └┘       └┘         └┘       └─────┘
st   ───┘└─────────────────┘└───────────┘└─────────┘└───────┘└─────┘└─
 49      rcases hrn with ⟨y, hy, z, hz, hyz⟩, change y + z = r • i at hyz,
id              └─┘                                         
src      └─────┘   └───────────────────────┘  └─────┘     └─────┘
typ      └─────┘└─┘└───────────────────────┘  └─────┘ └─────┘
doc      └─────┘   └───────────────────────┘  └─────┘       └─────┘
txt      └─────┘   └───────────────────────┘  └─────┘       └─────┘
par      └─────┘   └───────────────────────┘  └─────┘       └─────┘
pid               └───────────────────────┘               └────┘
st   ──────────────────────────────────────┘└───────────────────────────┘└─
 50      rw mem_smul_span_singleton at hy, rcases hy with ⟨c, hci, rfl⟩,
id          └─────────────────────┘               └┘
src      └─┘└─────────────────────┘└────┘  └─────┘  └─────────────────┘
typ      └─┘└─────────────────────┘└────┘  └─────┘└┘└─────────────────┘
doc      └─┘                       └────┘  └─────┘  └─────────────────┘
txt      └─┘                       └────┘  └─────┘  └─────────────────┘
par      └─┘                       └────┘  └─────┘  └─────────────────┘
pid                               └────┘          └─────────────────┘
st   ───────────────────────────────────┘└────────────────────────────┘└─
 51      use r-c, split,
id            
src      └──┘     └───┘
typ      └──┘   └───┘
doc      └──┘     └───┘
txt      └──┘     └───┘
par      └──┘     └───┘
pid         
st   ──────────┘└─────┘└─
 52      { rw [sub_right_comm], exact I.sub_mem hr1 hci },
id             └────────────┘         └───────┘ └─┘ └─┘
src        └──┘└────────────┘  └────┘└───────┘      
typ        └──┘└────────────┘  └────┘└───────┘└─┘└─┘
doc        └──┘                └────┘               
txt        └──┘                └────┘               
par        └──┘                └────┘               
pid          └┘                                    
st   ─────┘└────────────────┘└─────────────────────────┘└┘
 53      { rw [sub_smul, ← hyz, add_sub_cancel'], exact hz } },
id             └──────┘    └─┘  └─────────────┘         └┘
src        └──┘└──────┘└──┘   └┘└─────────────┘  └────┘  
typ        └──┘└──────┘└──┘└─┘└┘└─────────────┘  └────┘└┘
doc        └──┘        └──┘   └┘                 └────┘  
txt        └──┘        └──┘   └┘                 └────┘  
par        └──┘        └──┘   └┘                 └────┘  
pid          └┘        └──┘   └┘                        
st   ─────────────────┘└─────┘└───────────────┘└──────────┘└──┘
 54    rcases this with ⟨c, hc1, hci⟩, refine ⟨c * r, _, _, hs.2⟩,
id            └──┘                                       └┘
src    └─────┘    └─────────────────┘  └─────┘   └──────┘  └─┘
typ    └─────┘└──┘└─────────────────┘  └─────┘ └──────┘└┘└─┘
doc    └─────┘    └─────────────────┘  └─────┘    └──────┘  └─┘
txt    └─────┘    └─────────────────┘  └─────┘    └──────┘  └─┘
par    └─────┘    └─────────────────┘  └─────┘    └──────┘  └─┘
pid              └─────────────────┘            └──────┘  └─┘
st   ───────────────────────────────┘└──────────────────────────┘└─
 55    { rw [← ideal.quotient.eq, ideal.quotient.mk_one] at hr1 hc1 ⊢,
id             └───────────────┘  └───────────────────┘
src      └────┘└───────────────┘└┘└───────────────────┘└────────────┘
typ      └────┘└───────────────┘└┘└───────────────────┘└────────────┘
doc      └────┘                 └┘                     └────────────┘
txt      └────┘                 └┘                     └────────────┘
par      └────┘                 └┘                     └────────────┘
pid        └──┘                 └┘                     └───────────┘
st   ───┘└─────────────────────┘└─────────────────────┘└───────────┘└─
 56      rw [ideal.quotient.mk_mul, hc1, hr1, mul_one] },
id           └───────────────────┘  └─┘  └─┘  └─────┘
src      └──┘└───────────────────┘└┘   └┘   └┘└─────┘└┘
typ      └──┘└───────────────────┘└┘└─┘└┘└─┘└┘└─────┘└┘
doc      └──┘                     └┘   └┘   └┘       └┘
txt      └──┘                     └┘   └┘   └┘       └┘
par      └──┘                     └┘   └┘   └┘       └┘
pid        └┘                     └┘   └┘   └┘       
st   ────────────────────────────┘└───┘└───┘└───────┘└┘
 57    { intros n hn, specialize hrn hn, rw [mem_coe, mem_comap, mem_sup] at hrn,
id                               └─┘ └┘      └─────┘  └───────┘  └─────┘
src      └─────────┘  └─────────┘       └──┘└─────┘└┘└───────┘└┘└─────┘└──────┘
typ      └─────────┘  └─────────┘└─┘└┘  └──┘└─────┘└┘└───────┘└┘└─────┘└──────┘
doc      └─────────┘  └─────────┘       └──┘       └┘         └┘       └──────┘
txt      └─────────┘  └─────────┘       └──┘       └┘         └┘       └──────┘
par      └─────────┘  └─────────┘       └──┘       └┘         └┘       └──────┘
pid            └───┘                     └┘       └┘         └┘       └─────┘
st   ──────────────┘└─────────────────┘└───────────┘└─────────┘└───────┘└─────┘└─
 58      rcases hrn with ⟨y, hy, z, hz, hyz⟩, change y + z = r • n at hyz,
id              └─┘                                           
src      └─────┘   └───────────────────────┘  └─────┘       └─────┘
typ      └─────┘└─┘└───────────────────────┘  └─────┘   └─────┘
doc      └─────┘   └───────────────────────┘  └─────┘       └─────┘
txt      └─────┘   └───────────────────────┘  └─────┘       └─────┘
par      └─────┘   └───────────────────────┘  └─────┘       └─────┘
pid               └───────────────────────┘               └────┘
st   ──────────────────────────────────────┘└───────────────────────────┘└─
 59      rw mem_smul_span_singleton at hy, rcases hy with ⟨d, hdi, rfl⟩,
id          └─────────────────────┘               └┘
src      └─┘└─────────────────────┘└────┘  └─────┘  └─────────────────┘
typ      └─┘└─────────────────────┘└────┘  └─────┘└┘└─────────────────┘
doc      └─┘                       └────┘  └─────┘  └─────────────────┘
txt      └─┘                       └────┘  └─────┘  └─────────────────┘
par      └─┘                       └────┘  └─────┘  └─────────────────┘
pid                               └────┘          └─────────────────┘
st   ───────────────────────────────────┘└────────────────────────────┘└─
 60      change _ • _ ∈ I • span R s,
id                         └──┘  
src      └───────┘ └─┘   └──┘ 
typ      └───────┘ └─┘  └──┘
doc      └───────┘ └─┘   └──┘ 
txt      └───────┘ └─┘        
par      └───────┘ └─┘        
pid            └─┘ └─┘        
st   ──────────────────────────────┘└─
 61      rw [mul_smul, ← hyz, smul_add, smul_smul, mul_comm, mul_smul],
id           └──────┘    └─┘  └──────┘  └───────┘  └──────┘  └──────┘
src      └──┘└──────┘└──┘   └┘└──────┘└┘└───────┘└┘└──────┘└┘└──────┘
typ      └──┘└──────┘└──┘└─┘└┘└──────┘└┘└───────┘└┘└──────┘└┘└──────┘
doc      └──┘        └──┘   └┘        └┘         └┘        └┘        
txt      └──┘        └──┘   └┘        └┘         └┘        └┘        
par      └──┘        └──┘   └┘        └┘         └┘        └┘        
pid        └┘        └──┘   └┘        └┘         └┘        └┘        
st   ───────────────┘└─────┘└────────┘└─────────┘└────────┘└────────┘└──
 62      exact add_mem _ (smul_mem _ _ hci) (smul_mem _ _ hz) }
id             └─────┘                 └─┘   └──────┘     └┘
src      └────┘└─────┘└─┘         └───┘   └┘ └──────┘└───┘  └┘
typ      └────┘└─────┘└─┘         └───┘└─┘└┘ └──────┘└───┘└┘└┘
doc      └────┘       └─┘         └───┘   └┘         └───┘  └┘
txt      └────┘       └─┘         └───┘   └┘         └───┘  └┘
par      └────┘       └─┘         └───┘   └┘         └───┘  └┘
pid                  └─┘         └───┘   └┘         └───┘  
st   ────────────────────────────────────────────────────────┘└─
 63  end
st   ──┘
 64  
 65  theorem fg_bot : (⊥ : submodule α β).fg :=
id                        └───────┘   └┘
src                       └───────┘     └┘
typ                       └───────┘   └┘
doc                        └───────┘
 66  ⟨∅, by rw [finset.coe_empty, span_empty]⟩
id             └──────────────┘  └────────┘
src        └──┘└──────────────┘└┘└────────┘
typ        └──┘└──────────────┘└┘└────────┘
doc         └──┘                └┘          
txt         └──┘                └┘          
par         └──┘                └┘          
pid           └┘                └┘          
st         └───────────────────┘└──────────┘
 67  
 68  theorem fg_sup {s₁ s₂ : submodule α β}
id                           └───────┘  
src                          └───────┘
typ                          └───────┘  
doc                          └───────┘
 69    (hs₁ : s₁.fg) (hs₂ : s₂.fg) : (s₁ ⊔ s₂).fg :=
id            └┘└─┘         └┘└─┘     └┘  └┘ └┘
src             └─┘           └─┘            └┘
typ           └┘└─┘         └┘└─┘     └┘  └┘ └┘
 70  let ⟨t₁, ht₁⟩ := fg_def.1 hs₁, ⟨t₂, ht₂⟩ := fg_def.1 hs₂ in
id   └─┘  └┘  └─┘     └────┘  └─┘   └┘  └─┘     └────┘  └─┘
src                   └────┘                    └────┘
typ  └─┘  └┘  └─┘     └────┘  └─┘   └┘  └─┘     └────┘  └─┘
 71  fg_def.2 ⟨t₁ ∪ t₂, finite_union ht₁.1 ht₂.1, by rw [span_union, ht₁.2, ht₂.2]⟩
id   └────┘           └──────────┘                   └────────┘  └─┘    └─┘
src  └────┘           └──────────┘               └──┘└────────┘└┘   └──┘   └─┘
typ  └────┘           └──────────┘               └──┘└────────┘└┘└─┘└──┘└─┘└─┘
doc                                                  └──┘          └┘   └──┘   └─┘
txt                                                  └──┘          └┘   └──┘   └─┘
par                                                  └──┘          └┘   └──┘   └─┘
pid                                                    └┘          └┘   └──┘   └─┘
st                                                  └─────────────┘└───┘└─────┘└─┘
 72  
 73  variables {γ : Type*} [add_comm_group γ] [module α γ]
id                          └────────────┘     └────┘
src                         └────────────┘     └────┘
typ                         └────────────┘     └────┘
doc                                            └────┘
 74  variables {f : β →ₗ[α] γ}
id                    └─┘ 
src                   └─┘ 
typ                   └─┘ 
 75  
 76  theorem fg_map {s : submodule α β} (hs : s.fg) : (s.map f).fg :=
id                       └───────┘          └─┘     └──┘  └┘
src                      └───────┘             └─┘      └──┘   └┘
typ                      └───────┘          └─┘     └──┘  └┘
doc                      └───────┘                      └──┘
 77  let ⟨t, ht⟩ := fg_def.1 hs in fg_def.2 ⟨f '' t, finite_image _ ht.1, by rw [span_image, ht.2]⟩
id   └─┘    └┘     └────┘  └┘    └────┘    └┘    └──────────┘               └────────┘  └┘
src                 └────┘        └────┘     └┘    └──────────┘           └──┘└────────┘└┘  └─┘
typ  └─┘    └┘     └────┘  └┘    └────┘    └┘    └──────────┘           └──┘└────────┘└┘└┘└─┘
doc                                                                          └──┘          └┘  └─┘
txt                                                                          └──┘          └┘  └─┘
par                                                                          └──┘          └┘  └─┘
pid                                                                            └┘          └┘  └─┘
st                                                                          └─────────────┘└──┘└─┘
 78  
 79  theorem fg_prod {sb : submodule α β} {sc : submodule α γ}
id                         └───────┘          └───────┘  
src                        └───────┘            └───────┘
typ                        └───────┘          └───────┘  
doc                        └───────┘            └───────┘
 80    (hsb : sb.fg) (hsc : sc.fg) : (sb.prod sc).fg :=
id            └┘└─┘         └┘└─┘     └┘└───┘ └┘ └┘
src             └─┘           └─┘       └───┘    └┘
typ           └┘└─┘         └┘└─┘     └┘└───┘ └┘ └┘
doc                                     └───┘
 81  let ⟨tb, htb⟩ := fg_def.1 hsb, ⟨tc, htc⟩ := fg_def.1 hsc in
id   └─┘  └┘  └─┘     └────┘  └─┘   └┘  └─┘     └────┘  └─┘
src                   └────┘        └┘          └────┘
typ  └─┘  └┘  └─┘     └────┘  └─┘   └┘  └─┘     └────┘  └─┘
 82  fg_def.2 ⟨prod.inl '' tb ∪ prod.inr '' tc,
id   └────┘   └──────┘ └┘     └──────┘ └┘
src  └────┘   └──────┘ └┘     └──────┘ └┘
typ  └────┘   └──────┘ └┘     └──────┘ └┘
doc            └──────┘         └──────┘
 83    finite_union (finite_image _ htb.1) (finite_image _ htc.1),
id     └──────────┘  └──────────┘          └──────────┘      
src    └──────────┘  └──────────┘          └──────────┘      
typ    └──────────┘  └──────────┘          └──────────┘      
 84    by rw [linear_map.span_inl_union_inr, htb.2, htc.2]⟩
id            └───────────────────────────┘  └─┘    └─┘
src       └──┘└───────────────────────────┘└┘   └──┘   └─┘
typ       └──┘└───────────────────────────┘└┘└─┘└──┘└─┘└─┘
doc       └──┘                             └┘   └──┘   └─┘
txt       └──┘                             └┘   └──┘   └─┘
par       └──┘                             └┘   └──┘   └─┘
pid         └┘                             └┘   └──┘   └─┘
st       └────────────────────────────────┘└───┘└─────┘└─┘
 85  
 86  variable (f)
 87  /-- If 0 → M' → M → M'' → 0 is exact and M' and M'' are
 88  finitely generated then so is M. -/
 89  theorem fg_of_fg_map_of_fg_inf_ker {s : submodule α β}
id                                           └───────┘  
src                                          └───────┘
typ                                          └───────┘  
doc                                          └───────┘
 90    (hs1 : (s.map f).fg) (hs2 : (s ⊓ f.ker).fg) : s.fg :=
id             └──┘  └┘             └──┘ └┘     └─┘
src             └──┘   └┘               └──┘ └┘      └─┘
typ            └──┘  └┘             └──┘ └┘     └─┘
doc             └──┘                     └──┘
 91  begin
st   └─────
 92    haveI := classical.dec_eq α, haveI := classical.dec_eq β, haveI := classical.dec_eq γ,
id              └──────────────┘            └──────────────┘            └──────────────┘ 
src    └───────┘└──────────────┘   └───────┘└──────────────┘   └───────┘└──────────────┘
typ    └───────┘└──────────────┘  └───────┘└──────────────┘  └───────┘└──────────────┘
doc    └───────┘                   └───────┘                   └───────┘                
txt    └───────┘                   └───────┘                   └───────┘                
par    └───────┘                   └───────┘                   └───────┘                
pid         └─┘                        └─┘                        └─┘                
st   ────────────────────────────┘└───────────────────────────┘└───────────────────────────┘└─
 93    cases hs1 with t1 ht1, cases hs2 with t2 ht2,
id           └─┘                    └─┘
src    └────┘   └──────────┘  └────┘   └──────────┘
typ    └────┘└─┘└──────────┘  └────┘└─┘└──────────┘
doc    └────┘   └──────────┘  └────┘   └──────────┘
txt    └────┘   └──────────┘  └────┘   └──────────┘
par    └────┘   └──────────┘  └────┘   └──────────┘
pid            └──────────┘          └──────────┘
st   ──────────────────────┘└─────────────────────┘└─
 94    have : ∀ y ∈ t1, ∃ x ∈ s, f x = y,
id                  └┘           
src    └─────┘ └───┘   └───┘   
typ    └─────┘ └───┘└┘ └───┘ 
doc    └─────┘ └───┘    └───┘     
txt    └─────┘ └───┘    └───┘     
par    └─────┘ └───┘    └───┘     
pid    └───┘└┘ └───┘    └───┘     
st   ──────────────────────────────────┘└─
 95    { intros y hy,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid            └───┘
st   ───┘└─────────┘└─
 96      have : y ∈ map f s, { rw ← ht1, exact subset_span hy },
id                 └─┘           └─┘        └─────────┘ └┘
src      └─────┘  └─┘      └───┘     └────┘└─────────┘  
typ      └─────┘ └─┘    └───┘└─┘  └────┘└─────────┘└┘
doc      └─────┘  └─┘      └───┘     └────┘             
txt      └─────┘           └───┘     └────┘             
par      └─────┘           └───┘     └────┘             
pid      └───┘└┘             └─┘                       
st   ─────────────────────┘└──┘└──────┘└─────────────────────┘└┘
 97      rcases mem_map.1 this with ⟨x, hx1, hx2⟩,
id              └─────┘   └──┘
src      └─────┘└─────┘└─┘    └─────────────────┘
typ      └─────┘└─────┘└─┘└──┘└─────────────────┘
doc      └─────┘       └─┘    └─────────────────┘
txt      └─────┘       └─┘    └─────────────────┘
par      └─────┘       └─┘    └─────────────────┘
pid                   └─┘    └─────────────────┘
st   ───────────────────────────────────────────┘└─
 98      exact ⟨x, hx1, hx2⟩ },
id                └─┘  └─┘
src      └────┘  └┘   └┘   └┘
typ      └────┘ └┘└─┘└┘└─┘└┘
doc      └────┘  └┘   └┘   └┘
txt      └────┘  └┘   └┘   └┘
par      └────┘  └┘   └┘   └┘
pid             └┘   └┘   
st   ───────────────────────┘└┘
 99    have : ∃ g : γ → β, ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y,
id                          └┘           
src    └─────┘└───┘    └───┘            └┘ 
typ    └─────┘└───┘ └───┘└┘        └┘ 
doc    └─────┘ └───┘     └───┘            └┘ 
txt    └─────┘ └───┘     └───┘            └┘ 
par    └─────┘ └───┘     └───┘            └┘ 
pid    └───┘└┘ └───┘     └───┘            └┘ 
st   ────────────────────────────────────────────────────┘└─
100    { choose g hg1 hg2,
src      └──────────────┘
typ      └──────────────┘
doc      └──────────────┘
txt      └──────────────┘
par      └──────────────┘
pid            └┘└──────┘
st   ───┘└──────────────┘└─
101      existsi λ y, if H : y ∈ t1 then g y H else 0,
id                    └┘         └┘      
src      └──────┘ └──┘└┘└───┘    └────┘   └─────┘
typ      └──────┘ └──┘└┘└───┘  └┘└────┘  └─────┘
doc      └──────┘ └──┘  └───┘    └────┘   └─────┘
txt      └──────┘ └──┘  └───┘    └────┘   └─────┘
par      └──────┘ └──┘  └───┘    └────┘   └─────┘
pid              └──┘  └───┘    └────┘   └────┘
st   ───────────────────────────────────────────────┘└─
102      intros y H, split,
src      └────────┘  └───┘
typ      └────────┘  └───┘
doc      └────────┘  └───┘
txt      └────────┘  └───┘
par      └────────┘  └───┘
pid            └──┘
st   ─────────────┘└─────┘└─
103      { simp only [dif_pos H], apply hg1 },
id                    └─────┘ 
src        └─────────┘└─────┘   └────┘   
typ        └─────────┘└─────┘  └────┘   
doc        └─────────┘          └────┘   
txt        └─────────┘          └────┘   
par        └─────────┘          └────┘   
pid            └──┘└┘                  
st   ─────┘└───────────────────┘└──────────┘└┘
104      { simp only [dif_pos H], apply hg2 } },
id                    └─────┘ 
src        └─────────┘└─────┘   └────┘   
typ        └─────────┘└─────┘  └────┘   
doc        └─────────┘          └────┘   
txt        └─────────┘          └────┘   
par        └─────────┘          └────┘   
pid            └──┘└┘                  
st   ──────────────────────────┘└──────────┘└──┘
105    cases this with g hg, clear this,
id           └──┘
src    └────┘    └────────┘  └────────┘
typ    └────┘└──┘└────────┘  └────────┘
doc    └────┘    └────────┘  └────────┘
txt    └────┘    └────────┘  └────────┘
par    └────┘    └────────┘  └────────┘
pid             └────────┘       └───┘
st   ─────────────────────┘└──────────┘└─
106    existsi t1.image g ∪ t2,
id             └──────┘   └┘
src    └──────┘└──────┘ 
typ    └──────┘└──────┘└┘
doc    └──────┘└──────┘  
txt    └──────┘          
par    └──────┘          
pid                     
st   ────────────────────────┘└─
107    rw [finset.coe_union, span_union, finset.coe_image],
id         └──────────────┘  └────────┘  └──────────────┘
src    └──┘└──────────────┘└┘└────────┘└┘└──────────────┘
typ    └──┘└──────────────┘└┘└────────┘└┘└──────────────┘
doc    └──┘                └┘          └┘                
txt    └──┘                └┘          └┘                
par    └──┘                └┘          └┘                
pid      └┘                └┘          └┘                
st   ─────────────────────┘└──────────┘└────────────────┘└──
108    apply le_antisymm,
id           └─────────┘
src    └────┘└─────────┘
typ    └────┘└─────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ──────────────────┘└─
109    { refine sup_le (span_le.2 $ image_subset_iff.2 _) (span_le.2 _),
id              └────┘              └──────────────┘       └─────┘
src      └─────┘└────┘        └─┘ └──────────────┘└────┘ └─────┘└───┘
typ      └─────┘└────┘        └─┘ └──────────────┘└────┘ └─────┘└───┘
doc      └─────┘              └─┘ └──────────────┘└────┘        └───┘
txt      └─────┘              └─┘                 └────┘        └───┘
par      └─────┘              └─┘                 └────┘        └───┘
pid                          └─┘                 └────┘        └───┘
st   ───┘└────────────────────────────────────────────────────────────┘└─
110      { intros y hy, exact (hg y hy).1 },
id                             └┘  └┘
src        └─────────┘  └────┘      └──┘
typ        └─────────┘  └────┘ └┘└┘└──┘
doc        └─────────┘  └────┘      └──┘
txt        └─────────┘  └────┘      └──┘
par        └─────────┘  └────┘      └──┘
pid              └───┘             └─┘
st   ─────┘└─────────┘└──────────────────┘└┘
111      { intros x hx, have := subset_span hx,
id                              └─────────┘ └┘
src        └─────────┘  └──────┘└─────────┘
typ        └─────────┘  └──────┘└─────────┘└┘
doc        └─────────┘  └──────┘           
txt        └─────────┘  └──────┘           
par        └─────────┘  └──────┘           
pid              └───┘  └───┘└─┘           
st   ────────────────┘└──────────────────────┘└─
112        rw ht2 at this,
id            └─┘
src        └─┘   └──────┘
typ        └─┘└─┘└──────┘
doc        └─┘   └──────┘
txt        └─┘   └──────┘
par        └─┘   └──────┘
pid             └──────┘
st   ───────────────────┘└─
113        exact this.1 } },
id               └──┘
src        └────┘    └─┘
typ        └────┘└──┘└─┘
doc        └────┘    └─┘
txt        └────┘    └─┘
par        └────┘    └─┘
pid                 └─┘
st   ──────────────────┘└──┘
114    intros x hx,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid          └───┘
st   ────────────┘└─
115    have : f x ∈ map f s, { rw mem_map, exact ⟨x, hx, rfl⟩ },
id                 └─┘         └─────┘           └┘  └─┘
src    └─────┘   └─┘      └─┘└─────┘  └────┘  └┘  └┘└─┘└┘
typ    └─────┘  └─┘    └─┘└─────┘  └────┘ └┘└┘└┘└─┘└┘
doc    └─────┘   └─┘      └─┘         └────┘  └┘  └┘   └┘
txt    └─────┘            └─┘         └────┘  └┘  └┘   └┘
par    └─────┘            └─┘         └────┘  └┘  └┘   └┘
pid    └───┘└┘                              └┘  └┘   
st   ─────────────────────┘└──┘└────────┘└───────────────────┘└┘
116    rw [← ht1,← set.image_id ↑t1, finsupp.mem_span_iff_total] at this,
id           └─┘   └──────────┘ └┘  └────────────────────────┘
src    └────┘   └─┘└──────────┘  └┘└────────────────────────┘└───────┘
typ    └────┘└─┘└─┘└──────────┘└┘└┘└────────────────────────┘└───────┘
doc    └────┘   └─┘               └┘                          └───────┘
txt    └────┘   └─┘               └┘                          └───────┘
par    └────┘   └─┘               └┘                          └───────┘
pid      └──┘   └─┘               └┘                          └──────┘
st   ──────────┘└─────────────────┘└──────────────────────────┘└──────┘└─
117    rcases this with ⟨l, hl1, hl2⟩,
id            └──┘
src    └─────┘    └─────────────────┘
typ    └─────┘└──┘└─────────────────┘
doc    └─────┘    └─────────────────┘
txt    └─────┘    └─────────────────┘
par    └─────┘    └─────────────────┘
pid              └─────────────────┘
st   ───────────────────────────────┘└─
118    refine mem_sup.2 ⟨(finsupp.total β β α id).to_fun ((finsupp.lmap_domain α α g : (γ →₀ α) → β →₀ α) l), _,
id            └─────┘                                                                     └┘
src    └─────┘└─────┘└─┘                    └───────┘                        └─┘  └┘ └┘     └┘ └─────
typ    └─────┘└─────┘└─┘                    └───────┘                        └─┘  └┘ └┘     └┘ └─────
doc    └─────┘       └─┘                    └───────┘                        └─┘  └┘ └┘     └┘ └─────
txt    └─────┘       └─┘                    └───────┘                        └─┘     └┘     └┘ └─────
par    └─────┘       └─┘                    └───────┘                        └─┘     └┘     └┘ └─────
pid                 └─┘                    └───────┘                        └─┘     └┘     └┘ └─────
st   ────────────────────────────────────────────────────────────────────────────────────────────────────────────
119      x - finsupp.total β β α id ((finsupp.lmap_domain α α g : (γ →₀ α) → β →₀ α) l), _, add_sub_cancel'_right _ _⟩,
id         └───────────┘       └┘   └─────────────────┘                              └───────────────────┘
src  ───┘ └───────────┘   └┘  └─────────────────┘   └─┘     └┘     └┘ └────┘└───────────────────┘└───┘
typ  ───┘└───────────┘   └┘  └─────────────────┘ └─┘    └┘    └┘└────┘└───────────────────┘└───┘
doc  ───┘  └───────────┘                             └─┘     └┘     └┘ └────┘                     └───┘
txt  ───┘                                            └─┘     └┘     └┘ └────┘                     └───┘
par  ───┘                                            └─┘     └┘     └┘ └────┘                     └───┘
pid  ───┘                                            └─┘     └┘     └┘ └────┘                     └───┘
st   ────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
120    { rw [← set.image_id (g '' ↑t1), finsupp.mem_span_iff_total], refine ⟨_, _, rfl⟩,
id             └──────────┘   └┘  └┘   └────────────────────────┘                 └─┘
src      └────┘└──────────┘  └┘   └─┘└────────────────────────┘  └─────┘ └────┘└─┘
typ      └────┘└──────────┘ └┘ └┘└─┘└────────────────────────┘  └─────┘ └────┘└─┘
doc      └────┘                   └─┘                            └─────┘ └────┘   
txt      └────┘                   └─┘                            └─────┘ └────┘   
par      └────┘                   └─┘                            └─────┘ └────┘   
pid        └──┘                   └─┘                                   └────┘   
st   ───┘└───────────────────────────┘└──────────────────────────┘└───────────────────┘└─
121      haveI : inhabited γ := ⟨0⟩,
id               └───────┘ 
src      └──────┘└───────┘ └──┘ └┘
typ      └──────┘└───────┘└──┘ └┘
doc      └──────┘          └──┘ └┘
txt      └──────┘          └──┘ └┘
par      └──────┘          └──┘ └┘
pid           └┘          └──┘ └┘
st   ─────────────────────────────┘└─
122      rw [← finsupp.lmap_domain_supported _ _ g, mem_map],
id             └───────────────────────────┘       └─────┘
src      └────┘└───────────────────────────┘└───┘ └┘└─────┘
typ      └────┘└───────────────────────────┘└───┘└┘└─────┘
doc      └────┘                             └───┘ └┘       
txt      └────┘                             └───┘ └┘       
par      └────┘                             └───┘ └┘       
pid        └──┘                             └───┘ └┘       
st   ────────────────────────────────────────────┘└───────┘└──
123      refine ⟨l, hl1, _⟩,
id                 └─┘
src      └─────┘  └┘   └──┘
typ      └─────┘ └┘└─┘└──┘
doc      └─────┘  └┘   └──┘
txt      └─────┘  └┘   └──┘
par      └─────┘  └┘   └──┘
pid              └┘   └──┘
st   ─────────────────────┘└─
124      refl, },
src      └──┘
typ      └──┘
doc      └──┘
txt      └──┘
par      └──┘
st   ───────┘└──┘
125    rw [ht2, mem_inf], split,
id         └─┘  └─────┘
src    └──┘   └┘└─────┘  └───┘
typ    └──┘└─┘└┘└─────┘  └───┘
doc    └──┘   └┘         └───┘
txt    └──┘   └┘         └───┘
par    └──┘   └┘         └───┘
pid      └┘   └┘       
st   ────────┘└───────┘└──────┘└─
126    { apply s.sub_mem hx,
id             └───────┘ └┘
src      └────┘└───────┘
typ      └────┘└───────┘└┘
doc      └────┘         
txt      └────┘         
par      └────┘         
pid                    
st   ───┘└────────────────┘└─
127      rw [finsupp.total_apply, finsupp.lmap_domain_apply, finsupp.sum_map_domain_index],
id           └─────────────────┘  └───────────────────────┘  └──────────────────────────┘
src      └──┘└─────────────────┘└┘└───────────────────────┘└┘└──────────────────────────┘
typ      └──┘└─────────────────┘└┘└───────────────────────┘└┘└──────────────────────────┘
doc      └──┘                   └┘                         └┘                            
txt      └──┘                   └┘                         └┘                            
par      └──┘                   └┘                         └┘                            
pid        └┘                   └┘                         └┘                            
st   ──────────────────────────┘└─────────────────────────┘└────────────────────────────┘└──
128      refine s.sum_mem _,
id              └───────┘
src      └─────┘└───────┘└┘
typ      └─────┘└───────┘└┘
doc      └─────┘         └┘
txt      └─────┘         └┘
par      └─────┘         └┘
pid                     └┘
st   ─────────────────────┘└─
129      { intros y hy, exact s.smul_mem _ (hg y (hl1 hy)).1 },
id                            └────────┘    └┘   └─┘ └┘
src        └─────────┘  └────┘└────────┘└─┘          └───┘
typ        └─────────┘  └────┘└────────┘└─┘ └┘ └─┘└┘└───┘
doc        └─────────┘  └────┘          └─┘          └───┘
txt        └─────────┘  └────┘          └─┘          └───┘
par        └─────────┘  └────┘          └─┘          └───┘
pid              └───┘                 └─┘          └┘└─┘
st   ─────┘└─────────┘└─────────────────────────────────────┘└┘
130      { exact zero_smul _ }, { exact λ _ _ _, add_smul _ _ _ } },
id               └───────┘                       └──────┘
src        └────┘└───────┘└─┘     └────┘ └──────┘└──────┘└─────┘
typ        └────┘└───────┘└─┘     └────┘ └──────┘└──────┘└─────┘
doc        └────┘         └─┘     └────┘ └──────┘        └─────┘
txt        └────┘         └─┘     └────┘ └──────┘        └─────┘
par        └────┘         └─┘     └────┘ └──────┘        └─────┘
pid                      └┘           └──────┘        └────┘
st   ─────┘└────────────────┘└┘└───────────────────────────────┘└──┘
131    { rw [linear_map.mem_ker, f.map_sub, ← hl2],
id           └────────────────┘               └─┘
src      └──┘└────────────────┘└┘         └──┘   
typ      └──┘└────────────────┘└┘└───────┘└──┘└─┘
doc      └──┘                  └┘         └──┘   
txt      └──┘                  └┘         └──┘   
par      └──┘                  └┘         └──┘   
pid        └┘                  └┘         └──┘   
st   ─────────────────────────┘└─────────┘└─────┘└──
132      rw [finsupp.total_apply, finsupp.total_apply, finsupp.lmap_domain_apply],
id           └─────────────────┘  └─────────────────┘  └───────────────────────┘
src      └──┘└─────────────────┘└┘└─────────────────┘└┘└───────────────────────┘
typ      └──┘└─────────────────┘└┘└─────────────────┘└┘└───────────────────────┘
doc      └──┘                   └┘                   └┘                         
txt      └──┘                   └┘                   └┘                         
par      └──┘                   └┘                   └┘                         
pid        └┘                   └┘                   └┘                         
st   ──────────────────────────┘└───────────────────┘└─────────────────────────┘└──
133      rw [finsupp.sum_map_domain_index, finsupp.sum, finsupp.sum, f.map_sum],
id           └──────────────────────────┘  └─────────┘  └─────────┘
src      └──┘└──────────────────────────┘└┘└─────────┘└┘└─────────┘└┘         
typ      └──┘└──────────────────────────┘└┘└─────────┘└┘└─────────┘└┘└───────┘
doc      └──┘                            └┘└─────────┘└┘└─────────┘└┘         
txt      └──┘                            └┘           └┘           └┘         
par      └──┘                            └┘           └┘           └┘         
pid        └┘                            └┘           └┘           └┘         
st   ───────────────────────────────────┘└───────────┘└───────────┘└─────────┘└──
134      rw sub_eq_zero,
id          └─────────┘
src      └─┘└─────────┘
typ      └─┘└─────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ─────────────────┘└─
135      refine finset.sum_congr rfl (λ y hy, _),
id              └──────────────┘ └─┘
src      └─────┘└──────────────┘└─┘  └───────┘
typ      └─────┘└──────────────┘└─┘  └───────┘
doc      └─────┘                     └───────┘
txt      └─────┘                     └───────┘
par      └─────┘                     └───────┘
pid                                 └───────┘
st   ──────────────────────────────────────────┘└─
136      unfold id,
src      └───────┘
typ      └───────┘
doc      └───────┘
txt      └───────┘
par      └───────┘
pid            └─┘
st   ────────────┘└─
137      rw [f.map_smul, (hg y (hl1 hy)).2],
id                        └┘   └─┘ └┘
src      └──┘          └┘          └───┘
typ      └──┘└────────┘└┘ └┘ └─┘└┘└───┘
doc      └──┘          └┘          └───┘
txt      └──┘          └┘          └───┘
par      └──┘          └┘          └───┘
pid        └┘          └┘          └───┘
st   ─────────────────┘└───────────────┘└────
138      { exact zero_smul _ }, { exact λ _ _ _, add_smul _ _ _ } }
id               └───────┘                       └──────┘
src        └────┘└───────┘└─┘     └────┘ └──────┘└──────┘└─────┘
typ        └────┘└───────┘└─┘     └────┘ └──────┘└──────┘└─────┘
doc        └────┘         └─┘     └────┘ └──────┘        └─────┘
txt        └────┘         └─┘     └────┘ └──────┘        └─────┘
par        └────┘         └─┘     └────┘ └──────┘        └─────┘
pid                      └┘           └──────┘        └────┘
st   ─────┘└────────────────┘└┘└───────────────────────────────┘└───
139  end
st   ──┘
140  
141  end submodule
142  
143  class is_noetherian (α β) [ring α] [add_comm_group β] [module α β] : Prop :=
id                            └──┘    └────────────┘    └────┘  
src                             └──┘     └────────────┘     └────┘
typ                           └──┘    └────────────┘    └────┘  
doc                                                         └────┘
144  (noetherian : ∀ (s : submodule α β), s.fg)
id                       └───────┘     └─┘
src                       └───────┘        └─┘
typ                      └───────┘     └─┘
doc                       └───────┘
145  
146  section
147  variables {α : Type*} {β : Type*} {γ : Type*}
id             
typ            
148  variables [ring α] [add_comm_group β] [add_comm_group γ]
id              └──┘    └────────────┘     └────────────┘
src             └──┘     └────────────┘     └────────────┘
typ             └──┘    └────────────┘     └────────────┘
149  variables [module α β] [module α γ]
id              └────┘       └────┘
src             └────┘       └────┘
typ             └────┘       └────┘
doc             └────┘       └────┘
150  open is_noetherian
151  include α
152  
153  theorem is_noetherian_submodule {N : submodule α β} :
id                                        └───────┘  
src                                       └───────┘
typ                                       └───────┘  
doc                                       └───────┘
154    is_noetherian α N ↔ ∀ s : submodule α β, s ≤ N → s.fg :=
id     └───────────┘          └───────┘         └─┘
src    └───────────┘            └───────┘              └─┘
typ    └───────────┘          └───────┘         └─┘
doc                              └───────┘
155  ⟨λ ⟨hn⟩, λ s hs, have s ≤ N.subtype.range, from (N.range_subtype).symm ▸ hs,
id      └┘      └┘         └──────┘└────┘        └────────────┘ └──┘   └┘
src                            └──────┘└────┘         └────────────┘ └──┘  
typ     └┘      └┘         └──────┘└────┘        └────────────┘ └──┘   └┘
doc                                     └────┘
156    linear_map.map_comap_eq_self this ▸ submodule.fg_map (hn _),
id     └──────────────────────────┘ └──┘  └──────────────┘
src    └──────────────────────────┘       └──────────────┘
typ    └──────────────────────────┘ └──┘  └──────────────┘
157  λ h, ⟨λ s, submodule.fg_of_fg_map_of_fg_inf_ker N.subtype (h _ $ submodule.map_subtype_le _ _) $
id            └──────────────────────────────────┘ └──────┘       └──────────────────────┘
src             └──────────────────────────────────┘  └──────┘        └──────────────────────┘
typ           └──────────────────────────────────┘ └──────┘       └──────────────────────┘
doc             └──────────────────────────────────┘
158    by rw [submodule.ker_subtype, inf_bot_eq]; exact submodule.fg_bot⟩⟩
id            └───────────────────┘  └────────┘         └──────────────┘
src       └──┘└───────────────────┘└┘└────────┘  └────┘└──────────────┘
typ       └──┘└───────────────────┘└┘└────────┘  └────┘└──────────────┘
doc       └──┘                     └┘            └────┘
txt       └──┘                     └┘            └────┘
par       └──┘                     └┘            └────┘
pid         └┘                     └┘                 
st       └────────────────────────┘└──────────┘└──────────────────────┘
159  
160  theorem is_noetherian_submodule_left {N : submodule α β} :
id                                             └───────┘  
src                                            └───────┘
typ                                            └───────┘  
doc                                            └───────┘
161    is_noetherian α N ↔ ∀ s : submodule α β, (N ⊓ s).fg :=
id     └───────────┘          └───────┘        └┘
src    └───────────┘            └───────┘            └┘
typ    └───────────┘          └───────┘        └┘
doc                              └───────┘
162  is_noetherian_submodule.trans
id   └─────────────────────┘└────┘
src  └─────────────────────┘└────┘
typ  └─────────────────────┘└────┘
163  ⟨λ H s, H _ inf_le_left, λ H s hs, (inf_of_le_right hs) ▸ H _⟩
id            └─────────┘      └┘   └─────────────┘ └┘   
src              └─────────┘             └─────────────┘     
typ           └─────────┘      └┘   └─────────────┘ └┘   
164  
165  theorem is_noetherian_submodule_right {N : submodule α β} :
id                                              └───────┘  
src                                             └───────┘
typ                                             └───────┘  
doc                                             └───────┘
166    is_noetherian α N ↔ ∀ s : submodule α β, (s ⊓ N).fg :=
id     └───────────┘          └───────┘        └┘
src    └───────────┘            └───────┘            └┘
typ    └───────────┘          └───────┘        └┘
doc                              └───────┘
167  is_noetherian_submodule.trans
id   └─────────────────────┘└────┘
src  └─────────────────────┘└────┘
typ  └─────────────────────┘└────┘
168  ⟨λ H s, H _ inf_le_right, λ H s hs, (inf_of_le_left hs) ▸ H _⟩
id            └──────────┘      └┘   └────────────┘ └┘   
src              └──────────┘             └────────────┘     
typ           └──────────┘      └┘   └────────────┘ └┘   
169  
170  variable (β)
171  theorem is_noetherian_of_surjective (f : β →ₗ[α] γ) (hf : f.range = ⊤)
id                                             └─┘         └────┘  
src                                             └─┘            └────┘  
typ                                            └─┘         └────┘  
doc                                                             └────┘
172    [is_noetherian α β] : is_noetherian α γ :=
id      └───────────┘      └───────────┘  
src     └───────────┘        └───────────┘
typ     └───────────┘      └───────────┘  
173  ⟨λ s, have (s.comap f).map f = s, from linear_map.map_comap_eq_self $ hf.symm ▸ le_top,
id              └────┘  └─┘           └──────────────────────────┘   └┘└───┘  └────┘
src               └────┘   └─┘             └──────────────────────────┘     └───┘  └────┘
typ             └────┘  └─┘           └──────────────────────────┘   └┘└───┘  └────┘
doc               └────┘   └─┘
174  this ▸ submodule.fg_map $ noetherian _⟩
id   └──┘  └──────────────┘   └────────┘
src        └──────────────┘   └────────┘
typ  └──┘  └──────────────┘   └────────┘
175  variable {β}
176  
177  theorem is_noetherian_of_linear_equiv (f : β ≃ₗ[α] γ)
id                                               └─┘ 
src                                               └─┘ 
typ                                              └─┘ 
doc                                               └─┘ 
178    [is_noetherian α β] : is_noetherian α γ :=
id      └───────────┘      └───────────┘  
src     └───────────┘        └───────────┘
typ     └───────────┘      └───────────┘  
179  is_noetherian_of_surjective _ f.to_linear_map f.range
id   └─────────────────────────┘   └────────────┘ └────┘
src  └─────────────────────────┘    └────────────┘  └────┘
typ  └─────────────────────────┘   └────────────┘ └────┘
180  
181  instance is_noetherian_prod [is_noetherian α β]
id                                └───────────┘  
src                               └───────────┘
typ                               └───────────┘  
182    [is_noetherian α γ] : is_noetherian α (β × γ) :=
id      └───────────┘      └───────────┘     
src     └───────────┘        └───────────┘      
typ     └───────────┘      └───────────┘     
183  ⟨λ s, submodule.fg_of_fg_map_of_fg_inf_ker (linear_map.snd α β γ) (noetherian _) $
id        └──────────────────────────────────┘  └────────────┘      └────────┘
src        └──────────────────────────────────┘  └────────────┘         └────────┘
typ       └──────────────────────────────────┘  └────────────┘      └────────┘
doc        └──────────────────────────────────┘  └────────────┘
184  have s ⊓ linear_map.ker (linear_map.snd α β γ) ≤ linear_map.range (linear_map.inl α β γ),
id          └────────────┘  └────────────┘      └──────────────┘  └────────────┘   
src          └────────────┘  └────────────┘         └──────────────┘  └────────────┘
typ         └────────────┘  └────────────┘      └──────────────┘  └────────────┘   
doc           └────────────┘  └────────────┘          └──────────────┘  └────────────┘
185  from λ x ⟨hx1, hx2⟩, ⟨x.1, trivial, prod.ext rfl $ eq.symm $ linear_map.mem_ker.1 hx2⟩,
id                └─┘       └─────┘  └──────┘ └─┘   └─────┘   └────────────────┘
src                            └─────┘  └──────┘ └─┘   └─────┘   └────────────────┘
typ               └─┘       └─────┘  └──────┘ └─┘   └─────┘   └────────────────┘
186  linear_map.map_comap_eq_self this ▸ submodule.fg_map (noetherian _)⟩
id   └──────────────────────────┘ └──┘  └──────────────┘  └────────┘
src  └──────────────────────────┘       └──────────────┘  └────────┘
typ  └──────────────────────────┘ └──┘  └──────────────┘  └────────┘
187  
188  instance is_noetherian_pi {α ι : Type*} {β : ι → Type*} [ring α]
id                                                           └──┘ 
src                                                           └──┘
typ                                                          └──┘ 
189    [Π i, add_comm_group (β i)] [Π i, module α (β i)] [fintype ι]
id          └────────────┘           └────┘        └─────┘ 
src          └────────────┘              └────┘           └─────┘
typ         └────────────┘           └────┘        └─────┘ 
doc                                      └────┘           └─────┘
190    [∀ i, is_noetherian α (β i)] : is_noetherian α (Π i, β i) :=
id          └───────────┘         └───────────┘        
src          └───────────┘            └───────────┘
typ         └───────────┘         └───────────┘        
191  begin
st   └─────
192    haveI := classical.dec_eq ι,
id              └──────────────┘ 
src    └───────┘└──────────────┘
typ    └───────┘└──────────────┘
doc    └───────┘                
txt    └───────┘                
par    └───────┘                
pid         └─┘                
st   ────────────────────────────┘└─
193    suffices : ∀ s : finset ι, is_noetherian α (Π i : (↑s : set ι), β i),
id                      └────┘    └───────────┘             └─┘    
src    └─────────┘ └───┘└────┘  └───────────┘   └───┘  └─┘└─┘    
typ    └─────────┘ └───┘└────┘  └───────────┘  └───┘ └─┘└─┘  
doc    └─────────┘ └───┘└────┘                  └───┘   └─┘       
txt    └─────────┘ └───┘                        └───┘   └─┘       
par    └─────────┘ └───┘                        └───┘   └─┘       
pid    └───────┘└┘ └───┘                        └───┘   └─┘       
st   ─────────────────────────────────────────────────────────────────────┘└─
194    { letI := this finset.univ,
id               └──┘ └─────────┘
src      └──────┘    └─────────┘
typ      └──────┘└──┘└─────────┘
doc      └──────┘    └─────────┘
txt      └──────┘    
par      └──────┘    
pid          └─┘    
st   ───┘└──────────────────────┘└─
195      refine @is_noetherian_of_linear_equiv _ _ _ _ _ _ _ _
id               └───────────────────────────┘
src      └─────┘ └───────────────────────────┘└────────────────
typ      └─────┘ └───────────────────────────┘└────────────────
doc      └─────┘                              └────────────────
txt      └─────┘                              └────────────────
par      └─────┘                              └────────────────
pid                                          └────────────────
st   ──────────────────────────────────────────────────────────
196        ⟨_, _, _, _, _, _⟩ (this finset.univ),
id                             └──┘ └─────────┘
src  ─────┘ └────────────────┘     └─────────┘
typ  ─────┘ └────────────────┘ └──┘└─────────┘
doc  ─────┘ └────────────────┘     └─────────┘
txt  ─────┘ └────────────────┘                
par  ─────┘ └────────────────┘                
pid  ─────┘ └────────────────┘                
st   ──────────────────────────────────────────┘
197      { exact λ f i, f ⟨i, finset.mem_univ _⟩ },
id                            └─────────────┘
src        └────┘ └────┘   └┘└─────────────┘└──┘
typ        └────┘ └────┘   └┘└─────────────┘└──┘
doc        └────┘ └────┘   └┘               └──┘
txt        └────┘ └────┘   └┘               └──┘
par        └────┘ └────┘   └┘               └──┘
pid              └────┘   └┘               └─┘
st         └────────────────────────────────────┘
198      { intros, ext, refl },
src        └────┘  └─┘
typ        └────┘  └─┘
doc        └────┘  └─┘
txt        └────┘  └─┘
par        └────┘  └─┘
st         └────┘ └──┘       
199      { intros, ext, refl },
st                           
200      { exact λ f i, f i.1 },
st                            
201      { intro, ext i, cases i, refl },
st                                     
202      { intro, ext i, refl } },
st                            └──┘
203    intro s,
204    induction s using finset.induction with a s has ih,
id               
typ              
205    { split, intro s, convert submodule.fg_bot, apply eq_bot_iff.2,
206      intros x hx, refine (submodule.mem_bot α).2 _, ext i, cases i.2 },
id                                              
typ                                             
st                                                                       └┘
207    refine @is_noetherian_of_linear_equiv _ _ _ _ _ _ _ _
208      ⟨_, _, _, _, _, _⟩ (@is_noetherian_prod _ (β a) _ _ _ _ _ _ _ ih),
id                                                   
typ                                                  
209    { exact λ f i, or.by_cases (finset.mem_insert.1 i.2)
210        (λ h : i.1 = a, show β i.1, from (eq.rec_on h.symm f.1))
id                      
typ                     
211        (λ h : i.1 ∈ s, show β i.1, from f.2 ⟨i.1, h⟩) },
id                             
typ                            
st                                                        └┘
212    { intros f g, ext i, unfold or.by_cases, cases i with i hi,
213      rcases finset.mem_insert.1 hi with rfl | h,
214      { change _ = _ + _, simp only [dif_pos], refl },
st                                                     └┘
215      { change _ = _ + _, have : ¬i = a, { rintro rfl, exact has h },
id                                      
typ                                     
st                                                                    └┘
216        simp only [dif_neg this, dif_pos h], refl } },
id                            └──┘
typ                           └──┘
st                                                   └──┘
217    { intros c f, ext i, unfold or.by_cases, cases i with i hi,
218      rcases finset.mem_insert.1 hi with rfl | h,
219      { change _ = c • _, simp only [dif_pos], refl },
id                    
typ                   
st                                                     └┘
220      { change _ = c • _, have : ¬i = a, { rintro rfl, exact has h },
id                                     
typ                                    
st                                                                    └┘
221        simp only [dif_neg this, dif_pos h], refl } },
id                            └──┘
typ                           └──┘
st                                                   └──┘
222    { exact λ f, (f ⟨a, finset.mem_insert_self _ _⟩, λ i, f ⟨i.1, finset.mem_insert_of_mem i.2⟩) },
id                      
typ                     
st                                                                                                  └┘
223    { intro f, apply prod.ext,
224      { simp only [or.by_cases, dif_pos] },
st                                          └┘
225      { ext i, cases i with i his,
226        have : ¬i = a, { rintro rfl, exact has his },
id                    
typ                   
st                                                    └┘
227        dsimp only [or.by_cases], change i ∈ s at his,
id                                             
typ                                            
228        rw [dif_neg this, dif_pos his] } },
id                     └──┘
typ                    └──┘
st                                       └──┘
229    { intro f, ext i, cases i with i hi,
230      rcases finset.mem_insert.1 hi with rfl | h,
231      { simp only [or.by_cases, dif_pos], refl },
st                                                └┘
232      { have : ¬i = a, { rintro rfl, exact has h },
id                    
typ                   
st                                                  └┘
233        simp only [or.by_cases, dif_neg this, dif_pos h], refl } }
id                                         └──┘
typ                                        └──┘
st                                                                └───
234  end
st   ──┘
235  
236  end
237  
238  open is_noetherian submodule function
239  
240  theorem is_noetherian_iff_well_founded
241    {α β} [ring α] [add_comm_group β] [module α β] :
id            └┘       └──┘  └──┘  └┘           
src           └┘       └──┘  └──┘  └┘
typ           └┘       └──┘  └──┘  └┘           
242    is_noetherian α β ↔ well_founded ((>) : submodule α β → submodule α β → Prop) :=
id                                                                   
src                      
typ                                                                  
243  ⟨λ h, begin
244    apply order_embedding.well_founded_iff_no_descending_seq.2,
245    swap, { apply is_strict_order.swap },
st                                        └┘
246    rintro ⟨⟨N, hN⟩⟩,
247    let M := ⨆ n, N n,
id                
typ               
248    resetI,
249    rcases submodule.fg_def.1 (noetherian M) with ⟨t, h₁, h₂⟩,
250    have hN' : ∀ {a b}, a ≤ b → N a ≤ N b :=
id                    
src                    
typ                   
251      λ a b, (strict_mono.le_iff_le (λ _ _, hN.1)).2,
id                                       
typ                                      
252    have : t ⊆ ⋃ i, (N i : set β),
id                          └─┘ 
src                           └─┘
typ                         └─┘ 
253    { rw [← submodule.Union_coe_of_directed _ N _],
254      { show t ⊆ M, rw ← h₂,
id              
typ             
255        apply submodule.subset_span },
st                                     └┘
256      { apply_instance },
st                        └┘
257      { exact λ i j, ⟨max i j,
id                  
typ                 
258          hN' (le_max_left _ _),
259          hN' (le_max_right _ _)⟩ } },
st                                   └──┘
260    simp [subset_def] at this,
261    choose f hf using show ∀ x : t, ∃ (i : ℕ), x.1 ∈ N i, { simpa },
st                                                                   └┘
262    cases h₁ with h₁,
id           └┘
typ          └┘
263    let A := finset.sup (@finset.univ t h₁) f,
id                                       
typ                                      
264    have : M ≤ N A,
id                  
typ                 
265    { rw ← h₂, apply submodule.span_le.2,
266      exact λ x h, hN' (finset.le_sup (@finset.mem_univ t h₁ _))
id                                                        
typ                                                       
267        (hf ⟨x, h⟩) },
st                     └┘
268    exact not_le_of_lt (hN.1 (nat.lt_succ_self A))
id                                                
typ                                               
269      (le_trans (le_supr _ _) this)
270    end,
st     └─┘
271    begin
272      assume h, split, assume N,
273      suffices : ∀ M ≤ N, ∃ s, finite s ∧ M ⊔ submodule.span α s = N,
id                                                             
typ                                                            
274      { rcases this ⊥ bot_le with ⟨s, hs, e⟩,
275        exact submodule.fg_def.2 ⟨s, hs, by simpa using e⟩ },
id                                     └┘
typ                                    └┘
st                                                            └┘
276      refine λ M, h.induction M _, intros M IH MN,
277      letI := classical.dec,
id               └───────────┘
src              └───────────┘
typ              └───────────┘
278      by_cases h : ∀ x, x ∈ N → x ∈ M,
id                      
typ                     
279      { cases le_antisymm MN h, exact ⟨∅, by simp⟩ },
st                                                    └┘
280      { simp [not_forall] at h,
281        rcases h with ⟨x, h, h₂⟩,
282        have : ¬M ⊔ submodule.span α {x} ≤ M,
id                                      
typ                                     
283        { intro hn, apply h₂,
284          have := le_trans le_sup_right hn,
285          exact submodule.span_le.1 this (mem_singleton x) },
id                                                         
typ                                                        
st                                                            └┘
286        rcases IH (M ⊔ submodule.span α {x})
id                                         
typ                                        
287          ⟨@le_sup_left _ _ M _, this⟩
288          (sup_le MN (submodule.span_le.2 (by simpa))) with ⟨s, hs, hs₂⟩,
289        refine ⟨insert x s, finite_insert _ hs, _⟩,
id                                           └┘
typ                                          └┘
290        rw [← hs₂, sup_assoc, ← submodule.span_union], simp }
st                                                             └┘
291    end⟩
st     └─┘
292  
293  lemma well_founded_submodule_gt (α β) [ring α] [add_comm_group β] [module α β] :
id                                          └──┘     └──┘  └──┘  └┘            
src                                         └──┘     └──┘  └──┘  └┘
typ                                         └──┘     └──┘  └──┘  └┘            
294    ∀ [is_noetherian α β], well_founded ((>) : submodule α β → submodule α β → Prop) :=
id                                                                       
typ                                                                      
295  is_noetherian_iff_well_founded.mp
296  
297  lemma finite_of_linear_independent {α β} [nonzero_comm_ring α] [add_comm_group β] [module α β]
id                                              └┘ └┘ └┘ └┘ └┘     └┘  └──┘  └──┘            
src                                             └┘ └┘ └┘ └┘ └┘      └┘  └──┘  └──┘
typ                                             └┘ └┘ └┘ └┘ └┘     └┘  └──┘  └──┘            
doc                                             └┘ └┘ └┘ └┘ └┘
298    [is_noetherian α β] {s : set β} (hs : linear_independent α (subtype.val : s → β)) : s.finite :=
id                             └┘                                                     
src                              └┘
typ                            └┘                                                     
299  begin
300    refine classical.by_contradiction (λ hf, order_embedding.well_founded_iff_no_descending_seq.1
301      (well_founded_submodule_gt α β) ⟨_⟩),
302    have f : ℕ ↪ s, from @infinite.nat_embedding s ⟨λ f, hf ⟨f⟩⟩,
id                                                       └┘
src               
typ                                                      └┘
303    have : ∀ n, (subtype.val ∘ f) '' {m | m ≤ n} ⊆ s,
id                                                  
typ                                                 
304    { rintros n x ⟨y, hy₁, hy₂⟩, subst hy₂, exact (f y).2 },
id                                                      
typ                                                     
st                                                           └┘
305    have : ∀ a b : ℕ, a ≤ b ↔
306      span α ((subtype.val ∘ f) '' {m | m ≤ a}) ≤ span α ((subtype.val ∘ f) '' {m | m ≤ b}),
id                                                                               
typ                                                                              
307    { assume a b,
308      rw [span_le_span_iff (@zero_ne_one α _) hs (this a) (this b),
id                                                               
typ                                                              
309        set.image_subset_image_iff (injective_comp subtype.val_injective f.inj'),
310        set.subset_def],
311      exact ⟨λ hab x (hxa : x ≤ a), le_trans hxa hab, λ hx, hx a (le_refl a)⟩ },
id                └─┘                                                      
typ               └─┘                                                      
st                                                                               └┘
312    exact ⟨⟨λ n, span α ((subtype.val ∘ f) '' {m | m ≤ n}),
id                                              
typ                                             
313        λ x y, by simp [le_antisymm_iff, (this _ _).symm] {contextual := tt}⟩,
id                                                                        └┘
src                                                                         └┘
typ                                                                       └┘
314      by dsimp [gt]; simp only [lt_iff_le_not_le, (this _ _).symm]; tauto⟩
315  end
st   └─┘
316  
317  @[class] def is_noetherian_ring (α) [ring α] : Prop := is_noetherian α α
id                                        └──┘                             
src                                       └──┘
typ                                       └──┘                             
318  
319  instance is_noetherian_ring.to_is_noetherian {α : Type*} [ring α] :
id                                                             └┘   
src                                                            └┘
typ                                                            └┘   
320    ∀ [is_noetherian_ring α], is_noetherian α α := id
id                                             
typ                                            
321  
322  @[priority 80] -- see Note [lower instance priority]
323  instance ring.is_noetherian_of_fintype (R M) [fintype M] [ring R] [add_comm_group M] [module R M] : is_noetherian R M :=
id                                                 └─────┘    └──┘    └────────────┘                               
src                                                └─────┘     └──┘     └────────────┘
typ                                                └─────┘    └──┘    └────────────┘                               
doc                                                └─────┘
324  by letI := classical.dec; exact
id              └───────────┘
src             └───────────┘
typ             └───────────┘
325  ⟨assume s, ⟨to_finset s, by rw [finset.coe_to_finset', submodule.span_eq]⟩⟩
st                                                                           
326  
327  theorem ring.is_noetherian_of_zero_eq_one {R} [ring R] (h01 : (0 : R) = 1) : is_noetherian_ring R :=
id                                                  └──┘                                            
src                                                 └──┘
typ                                                 └──┘                                            
328  by haveI := subsingleton_of_zero_eq_one R h01;
id                                           
typ                                          
329     haveI := fintype.of_subsingleton (0:R);
id                                          
typ                                         
330     exact ring.is_noetherian_of_fintype _ _
331  
332  theorem is_noetherian_of_submodule_of_noetherian (R M) [ring R] [add_comm_group M] [module R M] (N : submodule R M)
id                                                           └┘      └──┘  └──┘  └┘                              
src                                                          └┘       └──┘  └──┘  └┘
typ                                                          └┘      └──┘  └──┘  └┘                              
333    (h : is_noetherian R M) : is_noetherian R N :=
id                                           
typ                                          
334  begin
335    rw is_noetherian_iff_well_founded at h ⊢,
336    convert order_embedding.well_founded (order_embedding.rsymm (submodule.map_subtype.lt_order_embedding N)) h
337  end
st   └─┘
338  
339  theorem is_noetherian_of_quotient_of_noetherian (R) [ring R] (M) [add_comm_group M] [module R M] (N : submodule R M)
id                                                        └┘          └──┘  └──┘  └┘                              
src                                                       └┘           └──┘  └──┘  └┘
typ                                                       └┘          └──┘  └──┘  └┘                              
340    (h : is_noetherian R M) : is_noetherian R N.quotient :=
id                                           
typ                                          
341  begin
342    rw is_noetherian_iff_well_founded at h ⊢,
343    convert order_embedding.well_founded (order_embedding.rsymm (submodule.comap_mkq.lt_order_embedding N)) h
344  end
st   └─┘
345  
346  theorem is_noetherian_of_fg_of_noetherian {R M} [ring R] [add_comm_group M] [module R M] (N : submodule R M)
id                                                    └┘       └──┘  └──┘  └┘                              
src                                                   └┘       └──┘  └──┘  └┘
typ                                                   └┘       └──┘  └──┘  └┘                              
347    [is_noetherian_ring R] (hN : N.fg) : is_noetherian R N :=
id                                                       
typ                                                      
348  let ⟨s, hs⟩ := hN in
349  begin
350    haveI := classical.dec_eq M,
id                               
typ                              
351    haveI := classical.dec_eq R,
id                               
typ                              
352    letI : is_noetherian R R := by apply_instance,
id                            
typ                           
353    have : ∀ x ∈ s, x ∈ N, from λ x hx, hs ▸ submodule.subset_span hx,
id                                  
typ                                 
354    refine @@is_noetherian_of_surjective ((↑s : set M) → R) _ _ _ (pi.module _)
id                                                └─┘     
src                                                └─┘
typ                                               └─┘     
355      _ _ _ is_noetherian_pi,
356    { fapply linear_map.mk,
357      { exact λ f, ⟨s.attach.sum (λ i, f i • i.1), N.sum_mem (λ c _, N.smul_mem _ $ this _ c.2)⟩ },
st                                                                                                  └┘
358      { intros f g, apply subtype.eq,
359        change s.attach.sum (λ i, (f i + g i) • _) = _,
360        simp only [add_smul, finset.sum_add_distrib], refl },
st                                                            └┘
361      { intros c f, apply subtype.eq,
362        change s.attach.sum (λ i, (c • f i) • _) = _,
id                                    
typ                                   
363        simp only [smul_eq_mul, mul_smul],
364        exact s.attach.sum_hom _ } },
st                                  └──┘
365    rw linear_map.range_eq_top,
366    rintro ⟨n, hn⟩, change n ∈ N at hn,
id                            
typ                           
367    rw [← hs, ← set.image_id ↑s, finsupp.mem_span_iff_total] at hn,
id                               
typ                              
368    rcases hn with ⟨l, hl1, hl2⟩,
369    refine ⟨λ x, l x.1, subtype.eq _⟩,
370    change s.attach.sum (λ i, l i.1 • i.1) = n,
id                                              
typ                                             
371    rw [@finset.sum_attach M M s _ (λ i, l i • i), ← hl2,
id                                     
typ                                    
372        finsupp.total_apply, finsupp.sum, eq_comm],
373    refine finset.sum_subset hl1 (λ x _ hx, _),
id                                     
typ                                    
374    rw [finsupp.not_mem_support_iff.1 hx, zero_smul]
st                                                    
375  end
st   └─┘
376  
377  /-- In a module over a noetherian ring, the submodule generated by finitely many vectors is
378  noetherian. -/
379  theorem is_noetherian_span_of_finite (R) {M} [ring R] [add_comm_group M] [module R M] [is_noetherian_ring R]
id                                                 └┘      └──┘  └──┘  └┘                                  
src                                                └┘       └──┘  └──┘  └┘
typ                                                └┘      └──┘  └──┘  └┘                                  
380    {A : set M} (hA : finite A) : is_noetherian R (submodule.span R A) :=
id          └┘                                                     
src         └┘
typ         └┘                                                     
381  is_noetherian_of_fg_of_noetherian _ (submodule.fg_def.mpr ⟨A, hA, rfl⟩)
id                                                                └┘
typ                                                               └┘
382  
383  theorem is_noetherian_ring_of_surjective (R) [comm_ring R] (S) [comm_ring S]
id                                                  └┘ └┘          └──┘  └┘ 
src                                                 └┘ └┘           └──┘  └┘
typ                                                 └┘ └┘          └──┘  └┘ 
384    (f : R → S) [is_ring_hom f] (hf : function.surjective f)
id                                                        
typ                                                       
385    [H : is_noetherian_ring R] : is_noetherian_ring S :=
id                                                    
typ                                                   
386  begin
387    unfold is_noetherian_ring at H ⊢,
388    rw is_noetherian_iff_well_founded at H ⊢,
389    convert order_embedding.well_founded (order_embedding.rsymm (ideal.lt_order_embedding_of_surjective f hf)) H
id                                                                                                          └┘
typ                                                                                                         └┘
390  end
st   └─┘
391  
392  instance is_noetherian_ring_range {R} [comm_ring R] {S} [comm_ring S] (f : R → S) [is_ring_hom f]
id                                          └──┘  └─┘         └┘ └┘ └┘                          
src                                         └──┘  └─┘          └┘ └┘ └┘
typ                                         └──┘  └─┘         └┘ └┘ └┘                          
393    [is_noetherian_ring R] : is_noetherian_ring (set.range f) :=
id                                                           
typ                                                          
394  @is_noetherian_ring_of_surjective R _ (set.range f) _ (λ x, ⟨f x, x, rfl⟩)
id                                                                 
typ                                                                
395    (⟨subtype.eq (is_ring_hom.map_one f),
id                                       
typ                                      
396      λ _ _, subtype.eq (is_ring_hom.map_mul f),
id                                            
typ                                           
397      λ _ _, subtype.eq (is_ring_hom.map_add f)⟩)
id                                            
typ                                           
398    (λ ⟨x, y, hy⟩, ⟨y, subtype.eq hy⟩) _
id              
typ             
399  
400  theorem is_noetherian_ring_of_ring_equiv (R) [comm_ring R] {S} [comm_ring S]
id                                                 └──┘  └─┘         └┘ └┘ └┘ 
src                                                └──┘  └─┘          └┘ └┘ └┘
typ                                                └──┘  └─┘         └┘ └┘ └┘ 
401    (f : R ≃+* S) [is_noetherian_ring R] : is_noetherian_ring S :=
id                                                            
typ                                                           
402  is_noetherian_ring_of_surjective R S f.1 f.to_equiv.surjective
id                                     
typ                                    
403  
404  namespace is_noetherian_ring
405  
406  variables {α : Type*} [integral_domain α] [is_noetherian_ring α]
id                           └┘ └┘ └┘ └┘ └┘
src                          └┘ └┘ └┘ └┘ └┘
typ                          └┘ └┘ └┘ └┘ └┘
407  open associates nat
408  
409  local attribute [elab_as_eliminator] well_founded.fix
doc                   └────────────────┘
410  
411  lemma well_founded_dvd_not_unit : well_founded (λ a b : α, a ≠ 0 ∧ ∃ x, ¬is_unit x ∧ b = a * x ) :=
id                                                                                       
src                                                                                   
typ                                                                                      
412  by simp only [ideal.span_singleton_lt_span_singleton.symm];
413     exact inv_image.wf (λ a, ideal.span ({a} : set α)) (well_founded_submodule_gt _ _)
id                                                └─┘ 
src                                                └─┘
typ                                               └─┘ 
414  
415  lemma exists_irreducible_factor {a : α} (ha : ¬ is_unit a) (ha0 : a ≠ 0) :
id                                                                  
src                                                
typ                                                                 
416    ∃ i, irreducible i ∧ i ∣ a :=
id                          
src                       
typ                         
417  (irreducible_or_factor a ha).elim (λ hai, ⟨a, hai, dvd_refl _⟩)
id                                             
typ                                            
418    (well_founded.fix
419      well_founded_dvd_not_unit
420      (λ a ih ha ha0 ⟨x, y, hx, hy, hxy⟩,
id                        
typ                       
421        have hx0 : x ≠ 0, from λ hx0, ha0 (by rw [← hxy, hx0, zero_mul]),
st                                                                       
422        (irreducible_or_factor x hx).elim
423          (λ hxi, ⟨x, hxi, hxy ▸ by simp⟩)
424          (λ hxf, let ⟨i, hi⟩ := ih x ⟨hx0, y, hy, hxy.symm⟩ hx hx0 hxf in
id                        
typ                       
425            ⟨i, hi.1, dvd.trans hi.2 (hxy ▸ by simp)⟩)) a ha ha0)
id                                                         
typ                                                        
426  
427  @[elab_as_eliminator] lemma irreducible_induction_on {P : α → Prop} (a : α)
id                                                                            
typ                                                                           
doc    └────────────────┘
428    (h0 : P 0) (hu : ∀ u : α, is_unit u → P u)
id                                         
typ                                        
429    (hi : ∀ a i : α, a ≠ 0 → irreducible i → P a → P (i * a)) :
id                                                      
typ                                                     
430    P a :=
id       
typ      
431  by haveI := classical.dec; exact
id               └───────────┘
src              └───────────┘
typ              └───────────┘
432  well_founded.fix well_founded_dvd_not_unit
433    (λ a ih, if ha0 : a = 0 then ha0.symm ▸ h0
id        
typ       
434      else if hau : is_unit a then hu a hau
435      else let ⟨i, hii, ⟨b, hb⟩⟩ := exists_irreducible_factor hau ha0 in
id                         
typ                        
436        have hb0 : b ≠ 0, from λ hb0, by simp * at *,
437        hb.symm ▸ hi _ _ hb0 hii (ih _ ⟨hb0, i,
438          hii.1, by rw [hb, mul_comm]⟩))
st                                     
439    a
id     
typ    
440  
441  lemma exists_factors (a : α) : a ≠ 0 →
id                                 
typ                                
442    ∃f:multiset α, (∀b∈f, irreducible b) ∧ associated a f.prod :=
id                                                    
src                                         
typ                                                   
443  is_noetherian_ring.irreducible_induction_on a
id                                               
typ                                              
444    (λ h, (h rfl).elim)
445    (λ u hu _, ⟨0, by simp [associated_one_iff_is_unit, hu]⟩)
id        
typ       
446    (λ a i ha0 hii ih hia0,
id         
typ        
447      let ⟨s, hs⟩ := ih ha0 in
id            
typ           
448      ⟨i::s, ⟨by clear _let_match; finish,
id        
typ       
449        by rw multiset.prod_cons;
450          exact associated_mul_mul (by refl) hs.2⟩⟩)
451  
452  end is_noetherian_ring
453  
454  namespace submodule
455  variables {R : Type*} {A : Type*} [comm_ring R] [ring A] [algebra R A]
id                                       └─┘ └─┘      └┘
src                                      └─┘ └─┘      └┘
typ                                      └─┘ └─┘      └┘
456  variables (M N : submodule R A)
457  
458  local attribute [instance] set.pointwise_mul_semiring
459  
460  theorem fg_mul (hm : M.fg) (hn : N.fg) : (M * N).fg :=
461  let ⟨m, hfm, hm⟩ := fg_def.1 hm, ⟨n, hfn, hn⟩ := fg_def.1 hn in
id                                     
typ                                    
462  fg_def.2 ⟨m * n, set.pointwise_mul_finite hfm hfn, span_mul_span R m n ▸ hm ▸ hn ▸ rfl⟩
id                                                                    
typ                                                                   
463  
464  lemma fg_pow (h : M.fg) (n : ℕ) : (M^n).fg :=
id                                       
src                               
typ                                      
465  nat.rec_on n
id              
typ             
466  (⟨finset.singleton 1, by simp [one_eq_span]⟩)
467  (λ n ih, by simpa [pow_succ] using fg_mul _ _ h ih)
id      
typ     
468  
469  end submodule